COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	uniqueness predicate
C00004 ENDMK
C⊗;
;uniqueness predicate
(wipe-out)
(proof foo)

(decl (var1 var2) (type: |?vartype|))
(decl (prd) (type: |@var1→truthval|))
(decl (unique) (type: |@prd→truthval|))
(define
 unique 
 |∀prd.unique(prd)=
	     ((∃var1.prd(var1))∧(∀var1 var2.prd(var1)∧prd(var2)⊃var1=var2))|)

(trw |unique(foo)| (open unique))
;FOO is unknown.
;the symbol FOO declared to have type (?VARTYPE)→TRUTHVAL
;UNIQUE(FOO)≡(∃VAR1.FOO(VAR1))∧(∀VAR1 VAR2.FOO(VAR1)∧FOO(VAR2)⊃VAR1=VAR2)
 
(trw |unique(λx.x=1)| (open unique))
;X is unknown.
;the symbol X declared to have type GROUND
;UNIQUE(λX.X=1)

(decl |∃!| (syntype: bindop) (type: |<?vartype>⊗truthval→truthval|))
(axiom |∀prd.(∃! var.prd(var))=unique(prd)|)
(label unique_def)
(label simpinfo)
 
(trw |∃! x.(x=1)|
     (open unique) (use unique_def mode: always ue: ((prd.|λx.x=1|)) ))
;∃! X.(X=1)
 
(trw |∃! x.foo(x)| (open unique))
;∃! X.(FOO(X))≡(∃VAR1.FOO(VAR1))∧(∀VAR1 VAR2.FOO(VAR1)∧FOO(VAR2)⊃VAR1=VAR2)

(trw |∃! x.foo(x)|)
;∃! X.(FOO(X))≡UNIQUE(FOO)